.\" Process this file with
.\" groff -man -Tascii cbmc.1
.\"
.TH CBMC 1 "MARCH 2012" "cbmc-4.1" "User Manual"
.SH NAME
cbmc \- Bounded Model Checker for C and C++ programs
.SH SYNOPSIS
.B cbmc [--claim \fIclaim-nr\fB] \fIfile.c\fB ...

.B cbmc [--show-claims] \fIfile.c\fB ...

.B cbmc [--all-claims] \fIfile.c\fB ...

.B goto-cc [-I \fIinclude-path\fB] [-c] \fIfile.c\fB [-o \fIoutfile.o\fB]

.B goto-instrument \fIinfile\fB \fIoutfile\fR

.PP
Only the most useful options are listed here; see below for the remainder.
.SH DESCRIPTION
\fBcbmc\fR generates traces that demonstrate how an assertion can be
violated, or proves that the assertion cannot be violated within a given
number of loop iterations.  CBMC can read source-code directly, or a
goto-binary generated by goto-cc.  Without any further options, cbmc checks
all properties (automatically generated or user-specificed) found in the
program.  If any of the properties can be violated, a counterexample is
printed and the analysis is aborted.  The analysis can be restricted to a
particular claim with the \-\-claim option.  The verification result for all
claims can be obtained by means of the \-\-all-claims option.

\fBgoto-cc\fR reads source code, and generates a goto-binary. It's
command-line interface is designed to mimic that of
.BR gcc (1).
Note in particular that \fBgoto-cc\fR distinguishes between compiling
and linking phases, just as gcc does. \fBcbmc\fR expects a goto-binary
for which linking has been completed.

\fBgoto-instrument\fR reads a goto-binary, performs a given program
transformation, and then writes the resulting program as goto-binary on
disc.

The usual flow is to (1) translate source into a goto-binary using
goto-cc, then (2) perform instrumentation with goto-instrument, and
finally (3) perform the analysis with cbmc.
.SH OPTIONS
.SS "FRONTEND OPTIONS (cbmc and goto-cc)"
.IP "-I path"
Set include path (C/C++)
.IP "-D macro"
Define preprocessor macro (C/C++)
.IP --preprocess
Stop after preprocessing
.IP --show-symbol-table
Show symbol table
.IP --show-goto-functions
Show goto program

.SS "ARCHITECTURAL OPTIONS (cbmc and goto-cc)"
\fBcbmc\fR by default uses architectural settings that match those of the
machine \fBcbmc\fR is executed on, i.e., the settings below are only needed
when verifying software that is meant to run on a different architecture
or OS. \fBgoto-cc\fR generates a goto-binary for a particular architecture,
i.e., the architecture cannot be changed after the goto-binary is generated.
.IP "--16, --32, --64"
Set width of int
.IP "--LP64, --ILP64, --LLP64, --ILP32, --LP32"
Set width of int, long and pointers
.IP --little-endian
Allow little-endian word-byte conversions
.IP --big-endian
Allow big-endian word-byte conversions
.IP --unsigned-char
Make "char" unsigned by default
.IP --ppc-macos
Set MACOS/PPC architecture
.IP --i386-macos
Set MACOS/I386 architecture
.IP --i386-linux
Set Linux/I386 architecture
.IP --i386-win32
Set Windows/I386 architecture
.IP --winx64
Set Windows/X64 architecture
.IP --no-arch
Don't set up an architecture
.IP --no-library
Disable built-in abstract C library
.IP "--round-to-nearest, --round-to-plus-inf, --round-to-minus-inf, --round-to-zero"
IEEE floating point rounding mode (default is round to nearest)
.SS "PROGRAM INSTRUMENTATION OPTIONS (cbmc and goto-instrument)"
Both \fBcbmc\fR and \fBgoto-instrument\fR can generate assertions that
catch specific common errors, as listed below.
.IP --bounds-check
Enable array bounds checks
.IP --div-by-zero-check
Enable division by zero checks
.IP --pointer-check
Enable pointer checks
.IP --signed-overflow-check
Enable arithmetic over- and underflow checks for signed integer arithmetic
.IP --unsigned-overflow-check
Enable arithmetic over- and underflow checks for unsigned integer arithmetic
.IP --nan-check
Check floating-point computations for NaN
.IP --no-assertions
Ignore user-provided assertions
.IP --no-assumptions
Ignore user-provided assumptions
.IP "--error-label label"
Check that the given label is unreachable
.SS "PROGRAM INSTRUMENTATION OPTIONS (goto-instrument only)"
\fBgoto-instrument\fR supports further, more complex, program
transformations.
.IP --nondet-volatile
Makes reads from volatile variables non-deterministic
.IP "--isr function"
Instruments an interrupt service routine with the given name
.IP --mmio
Instruments memory-mapped I/O
.IP --nondet-static
Variables with static lifetime are initialized non-deretministically
.IP --dump-c
Output ANSI-C source code instead of a goto binary.
.SS "BMC OPTIONS (cbmc)"
.IP --all-claims
Report status of all claims
.IP --show-claims
Only show claims
.IP --show-loops
Show the loops in the program
.IP --cover-assertions
Check which assertions are reachable
.IP "--function name"
Set main function name
.IP "--claim nr"
Only check specific claim
.IP --program-only
Only show program expression
.IP "--depth nr "
Limit search depth
.IP "--unwind nr "
Unwind loops nr times
.IP "--unwindset L:B,..."
Unwind loop L with a bound of B (use \-\-show\-loops to get the loop IDs)
.IP --show-vcc
Show the verification conditions
.IP --slice-formula
Remove assignments unrelated to property
.IP --no-unwinding-assertions
Do not generate unwinding assertions
.IP --no-pretty-names
Do not simplify identifiers
.SS "BACKEND OPTIONS (cbmc)"
.IP --dimacs
Generate CNF in DIMACS format for use by external SAT solvers
.IP --beautify-greedy
Beautify the counterexample (greedy heuristic)
.IP --smt1
Output subgoals in SMT1 syntax (experimental)
.IP --smt2
Output subgoals in SMT2 syntax (experimental)
.IP --boolector
Use Boolector (experimental)
.IP --mathsat
Use MathSAT (experimental)
.IP --cvc
Use CVC3 (experimental)
.IP --yices
Use Yices (experimental)
.IP --z3
Use Z3 (experimental)
.IP --refine
Use refinement procedure (experimental)
.IP "--outfile filename"
Output formula to given file
.IP --arrays-uf-never
Never turn arrays into uninterpreted functions
.IP --arrays-uf-always
Always turn arrays into uninterpreted functions
.SH ENVIRONMENT
CBMC does not regognize any environment variables. Note, however, that
the preprocessor used by CBMC will use environment variables to locate
header files. GOTO-CC aims to accept all environment variables that GCC
does.
.SH COPYRIGHT
2001-2012, Daniel Kroening, Edmund Clarke
